ds:x:Id fp Type, da:k:Knd fp Type, x:ecl(ds;da), m:, L:event-info(ds;da) List.
ecl-halt(ds;da;x)(m,L)  (m  0.ecl-ex(x)) 

latex

Definitions

x:A. B(x), , P  Q, ecl-ex(x), Prop, {T}, t  T, x. t(x), AB, A, False, S  T, if b t else f fi, P  Q, T, True, true, false, SQType(T), ecl-halt(ds;da;x), , x(s), P & Q, x:A. B(x), star-append(T;P;Q), P  Q, P  Q, Unit, Dec(P), A & B,

Lemmas

ecl-induction, nat wf, event-info wf, ecl-halt wf, l member wf, le wf, ecl-ex wf, nat plus inc, nat plus wf, ecl wf, member singleton, eclbase wf, decl-state wf, ma-valtype wf, bool wf, cons member, merge wf, member-merge, eclseq wf, ecland wf, eclor wf, eclrepeat wf, eclact wf, iff transitivity, eqtt to assert, assert of eq int, eqff to assert, assert of bnot, not functionality wrt iff, s-insert wf, member-s-insert, eclthrow wf, eclcatch wf, fpf wf, Knd wf, Id wf, decidable int equal